Recursive Functions

SMTLIB2 standard: Page 62

You can define recursive functions

Z3 unfolds the definition of recursive functions incrementally by iterative deepening: it attempts first to establish satisfiability modulo a fixed bound on number of unfoldings; if the resulting formula is unsatisfiable and the reason for unsatisfiability is due to the bound restriction, it increases the fixed bound incrementally. Note that this approach does not involve reasoning by induction that is often required to prove deeper properties of recursive functions. This scheme allows to decide satisfiability and unsatisfiability for a limited, but often useful, class of formulas.

Recognizing Quantified Definitions

Z3 5.3 adds the recfun-finder simplifier for inputs that encode recursive definitions as universally quantified equations, rather than using define-fun-rec. For example, it can recognize a definition whose left side is (f x) and whose right side contains a recursive call to f. Enable it explicitly in a set-simplifier pipeline, or with (set-option :smt.recfun_finder true) in the default solver pipeline.

This transformation uses the existing recursive-function machinery; it does not add induction or guarantee termination of recursive definitions. Prefer define-fun-rec when writing a definition directly. See Simplifiers for a quantified-definition example.

Mutually Recursive Functions

You can also define functions that are mutually recursive. The syntax requires to declare all functions first in one block, and then define the bodies of the recursive functions in a second block.